Inference at * 
Iof proof for Lemma Agatha Murder Puzzle (JProver)Lori2R:


  Agatha hates Charles & Agatha hates Agatha
  & (p:Person. p is richer than Agatha  The Butler hates p)
  & (p:Person. Agatha hates p  Charles hates p)
  & (p:Person. Agatha hates p  The Butler hates p)
  & (p:Person. p likes Agatha  p likes The Butler  p likes Charles)
  & (p, q:Person. p kills q  p is richer than q)
  & (p, q:Person. p kills q  p hates q)
   The Butler did not kill Agatha & Charles did not kill Agatha 

latex

 by Unfolds ``likes notkills`` 0 THEN impR THEN Repeat (andL 1) 

latex

 1: 
 1: 1. Agatha hates Charles
 1: 2. Agatha hates Agatha
 1: 3. p:Person. p is richer than Agatha  The Butler hates p
 1: 4. p:Person. Agatha hates p  Charles hates p
 1: 5. p:Person. Agatha hates p  The Butler hates p
 1: 6. p:Person. p hates Agatha  p hates The Butler  p hates Charles
 1: 7. p, q:Person. p kills q  p is richer than q
 1: 8. p, q:Person. p kills q  p hates q
 1:   The Butler kills Agatha & Charles kills Agatha
 .

Definitions

x likes y, x did not kill y, A, x kills y, x:A. B(x), P  Q, x:AB(x), x hates y, P & Q, x:AB(x)